<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Indenting3</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\begin{document}

</a><a id="63" class="Markup">\begin{code}</a>
<a id="76" class="Keyword">record</a> <a id="Sigma"></a><a id="83" href="Indenting3.html#83" class="Record">Sigma</a> <a id="89" class="Symbol">(</a><a id="90" href="Indenting3.html#90" class="Bound">A</a> <a id="92" class="Symbol">:</a> <a id="94" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="97" class="Symbol">)</a> <a id="99" class="Symbol">(</a><a id="100" href="Indenting3.html#100" class="Bound">B</a> <a id="102" class="Symbol">:</a> <a id="104" href="Indenting3.html#90" class="Bound">A</a> <a id="106" class="Symbol">→</a> <a id="108" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="111" class="Symbol">)</a> <a id="113" class="Symbol">:</a> <a id="115" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="119" class="Keyword">where</a>
  <a id="127" class="Keyword">constructor</a> <a id="_,_"></a><a id="139" href="Indenting3.html#139" class="InductiveConstructor Operator">_,_</a>
  <a id="145" class="Keyword">field</a>
    <a id="Sigma.proj₁"></a><a id="155" href="Indenting3.html#155" class="Field">proj₁</a> <a id="161" class="Symbol">:</a> <a id="163" href="Indenting3.html#90" class="Bound">A</a>
    <a id="Sigma.proj₂"></a><a id="169" href="Indenting3.html#169" class="Field">proj₂</a> <a id="175" class="Symbol">:</a> <a id="177" href="Indenting3.html#100" class="Bound">B</a> <a id="179" href="Indenting3.html#155" class="Field">proj₁</a>

<a id="186" class="Keyword">open</a> <a id="191" href="Indenting3.html#83" class="Module">Sigma</a> <a id="197" class="Keyword">public</a>
<a id="204" class="Markup">\end{code}</a><a id="214" class="Background">

\end{document}
</a></pre></body></html>